A:Type, B1, B2:(AType), eq:EqDecider(A), f:a:A fp B1(a), g:a:A fp B2(a). f  f  g 

latex

Definitions	x:A. B(x), x  dom(f), t  T, b, P  Q, x. t(x), x(s), Top, a:A fp B(a), P  Q, P  Q, P & Q, P  Q, f(x), f  g, A & B, f  g, EqDecider(T)
Lemmas	fpf wf, deq wf, fpf-join-ap-left, fpf-ap wf, fpf-join-dom2, fpf-trivial-subtype-top, assert wf, fpf-dom wf